| Definitions | #$n, ||as||, e   X, (x l), False, e c e',   x. t(x), first(e), pred(e), x,y. t(x;y), pred!(e;e'),  , SWellFounded(R(x;y)), constant_function(f;A;B), e < e', r s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  , Msg(M), kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), EOrderAxioms(E; pred?; info), IdLnk, Unit, EqDecider(T),  , EState(T), Atom$n, loc(e), f(a), Top, x before y l, y=f*(x) via L, no_repeats(T;l), adjacent(T;L;x;y), L1  L2, hd(l), P & Q,  A, a < b, P  Q, Id,  x:A. B(x), left + right, x:A  B(x), type List, <a, b>,  , chain-consistent(f;chain), sys-antecedent(es;Sys), AbsInterface(A), Type, ES, P   Q, strong-subtype(A;B), a:A fp B(a),  x:A. B(x), x:A B(x), t.1, let x,y = A in B(x;y), E(X), {x:A| B(x)} , s = t, x << y, y is f*(x), E,  b, t T, last(L), (last change to x before e), lastchange(x;e), isrcv(k), es-first-from(es;e;l;tg), kind(e), isrcv(e), e loc e' , P  Q, P Q, es-init(es;e), destination(l), source(l), (e <loc e'), {T}, !Void(), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y),  T, True, first(e), SQType(T), s ~ t, f(x)?z, inl x , tt, inr x , ff |
